es:ES, i:Id, P:({e:E| loc(e) = i }Prop).
e@i. P(e)  e@i. first(e)  P(e) & e@i. first(e)  P(pred(e))  P(e) 

latex

Definitions	Dec(P), P  Q, WellFnd{i}(A;x,y.R(x;y)), {T}, (e <loc e'), P  Q, P  Q, P & Q, first(e), e@i. P(e), x. t(x), A, b, x(s), pred(e), P  Q, E, loc(e), x:A. B(x), Prop, Id, t  T, ES
Lemmas	event system wf, Id wf, es-loc wf, es-E wf, es-pred wf, assert wf, not wf, alle-at wf, es-first wf, es-loc-pred, es-locl wf, es-locl-wellfnd, decidable assert, es-pred-locl